$\forall$$T$:Type, ${\it as}$, ${\it bs}$:($T$ List). no\_repeats($T$;${\it as}$ @ ${\it bs}$) $\Leftarrow\!\Rightarrow$ no\_repeats($T$;${\it bs}$ @ ${\it as}$)